(*
** Definicion del lenguaje.
** Modulo de tipos y modulo con sintaxis y semantica del lenguaje.
*)

Require Import Arith.EqNat.
Set Implicit Arguments.


Module Type Types.

(** Tipos de datos *)
Parameter Bool    : Set.
Parameter Integer : Set.
Parameter Byte    : Set.
Parameter Matrix  : Set -> Integer -> Integer -> Set.

(** Constantes *)
Parameter TRUE  : Bool.
Parameter FALSE : Bool.

Parameter ONE  : Integer.
Parameter ZERO : Integer.

(** Operaciones sobre Bool *)
Parameter bool_not : Bool -> Bool.
Parameter bool_and : Bool -> Bool -> Bool.
Parameter bool_or  : Bool -> Bool -> Bool.

(** Operaciones sobre Integer *)
Parameter int_plus   : Integer -> Integer -> Integer.
Parameter int_minus  : Integer -> Integer -> Integer.
Parameter int_mult   : Integer -> Integer -> Integer.
Parameter int_div    : Integer -> Integer -> Integer.
Parameter int_modulo : Integer -> Integer -> Integer.
Parameter int_eq     : Integer -> Integer -> Bool.
Parameter int_lt     : Integer -> Integer -> Bool.
Parameter int_le     : Integer -> Integer -> Bool.
Parameter int_gt     : Integer -> Integer -> Bool.
Parameter int_ge     : Integer -> Integer -> Bool.

(** Operaciones sobre Byte *)
Parameter byte_shl : Byte -> Integer -> Byte.
Parameter byte_shr : Byte -> Integer -> Byte.
Parameter byte_xor : Byte -> Byte -> Byte.
Parameter byte_and : Byte -> Byte -> Byte.
Parameter byte_gt  : Byte -> Byte -> Bool.
Parameter byte_eq  : Byte -> Byte -> Bool.

(** Operaciones sobre Matrix *)
Parameter matrix_get  : forall A m n, Integer -> Integer -> Matrix A m n -> option A.
Parameter matrix_set  : forall A m n, Matrix A m n -> Integer -> Integer -> A -> option (Matrix A m n).
Parameter matrix_zero : forall (A: Set)(a: A) m n, Matrix A m n.

End Types.


Module Lang (types_impl: Types).
Import types_impl.

Inductive Id : Set := id : nat -> Id.
Definition equal_id (i i': Id) :=
  match (i, i') with
    (id n, id n') => beq_nat n n'
  end
.

(* Expresiones aritmeticas *)
Inductive ArithExp : Set := 
  | arith_exp_num   : Integer  -> ArithExp
  | arith_exp_id    : Id       -> ArithExp
  | arith_exp_plus  : ArithExp -> ArithExp -> ArithExp
  | arith_exp_minus : ArithExp -> ArithExp -> ArithExp
  | arith_exp_mult  : ArithExp -> ArithExp -> ArithExp
  | arith_exp_div   : ArithExp -> ArithExp -> ArithExp
  | arith_exp_mod   : ArithExp -> ArithExp -> ArithExp
.

Infix "+" := arith_exp_plus  (at level 50, left associativity) : lang_scope.
Infix "-" := arith_exp_minus (at level 50, left associativity) : lang_scope.
Infix "*" := arith_exp_mult  (at level 40, left associativity) : lang_scope.
Infix "/" := arith_exp_div   (at level 40, left associativity) : lang_scope.
Infix "mod" := arith_exp_mod (at level 40) : lang_scope.

Coercion arith_exp_num : Integer >-> ArithExp.
Coercion arith_exp_id  : Id      >-> ArithExp.

(* Expresiones de matrices *)
Inductive MatrixExp : Type :=
  | matrix_exp_init : ArithExp -> ArithExp -> MatrixExp
  | matrix_exp_lit  : forall A m n, Matrix A m n -> MatrixExp
  | matrix_exp_id   : Id -> MatrixExp
.

Coercion matrix_exp_lit : Matrix >-> MatrixExp.
Coercion matrix_exp_id  : Id >-> MatrixExp.

(* Expresiones de bytes *)
Inductive ByteExp : Type :=
  | byte_exp_num    : Byte      -> ByteExp
  | byte_exp_id     : Id        -> ByteExp
  | byte_exp_xor    : ByteExp   -> ByteExp  -> ByteExp
  | byte_exp_andbb  : ByteExp   -> ByteExp  -> ByteExp
  | byte_exp_shiftl : ByteExp   -> ArithExp -> ByteExp
  | byte_exp_shiftr : ByteExp   -> ArithExp -> ByteExp
  | byte_exp_matrix : MatrixExp -> ArithExp -> ArithExp -> ByteExp
.

Infix "xor" := byte_exp_xor    (at level 55, left associativity) : lang_scope.
Infix "band" := byte_exp_andbb (at level 55, left associativity) : lang_scope.
Infix "shl" := byte_exp_shiftl (at level 60, no associativity)   : lang_scope.
Infix "shr" := byte_exp_shiftr (at level 60, no associativity)   : lang_scope.
Notation "m [ i ][ j ]" := (byte_exp_matrix m i j) (at level 30) : lang_scope.

Coercion byte_exp_num : Byte >-> ByteExp.
Coercion byte_exp_id  : Id   >-> ByteExp.

(* Expresiones booleanas *)
Inductive BoolExp : Type := 
  | bool_exp_lit : Bool     -> BoolExp
  | bool_exp_id  : Id       -> BoolExp
  | bool_exp_not : BoolExp  -> BoolExp
  | bool_exp_eq  : ArithExp -> ArithExp -> BoolExp
  | bool_exp_lt  : ArithExp -> ArithExp -> BoolExp
  | bool_exp_le  : ArithExp -> ArithExp -> BoolExp
  | bool_exp_gt  : ArithExp -> ArithExp -> BoolExp
  | bool_exp_gtb : ByteExp  -> ByteExp  -> BoolExp
  | bool_exp_eqb : ByteExp  -> ByteExp  -> BoolExp
  | bool_exp_ge  : ArithExp -> ArithExp -> BoolExp
  | bool_exp_and : BoolExp  -> BoolExp  -> BoolExp
  | bool_exp_or  : BoolExp  -> BoolExp  -> BoolExp
.

Infix "==" := bool_exp_eq    (at level 75) : lang_scope.
Infix "lt" := bool_exp_lt    (at level 70) : lang_scope.
Infix "le" := bool_exp_le    (at level 70) : lang_scope.
Infix "gt" := bool_exp_gt    (at level 70) : lang_scope.
Infix "ge" := bool_exp_ge    (at level 70) : lang_scope.
Infix "gtb" := bool_exp_gtb  (at level 70) : lang_scope.
Notation "!" := bool_exp_not (at level 60) : lang_scope.
Infix "and" := bool_exp_and  (at level 65) : lang_scope.
Infix "or" := bool_exp_or    (at level 65) : lang_scope.
Infix "b==" := bool_exp_eqb   (at level 70) : lang_scope.

Coercion bool_exp_id  : Id   >-> BoolExp.
Coercion bool_exp_lit : Bool >-> BoolExp.

(* Valores en almacenados en el estado *)
Inductive Val : Type :=
  | bool_val        : Bool    -> Val
  | int_val         : Integer -> Val
  | byte_val        : Byte    -> Val
  | byte_matrix_val : forall m n, Matrix Byte m n -> Val
.

(* Estado *)
Definition State := Id -> option Val.
Definition empty_state : State := fun _ => None.
Definition update(st: State)(id: Id)(val: Val) : State :=
  fun (id': Id) => if (equal_id id id') then Some val else st id'.

Open Scope lang_scope.

(* Evaluacion de expresiones aritmeticas *)
Inductive ArithEval (st: State) : ArithExp -> Integer -> Prop :=
  | arith_eval_num : forall (z: Integer),
      ArithEval st (arith_exp_num z) z

  | arith_eval_id : forall (i: Id)(z: Integer),
      st i = Some (int_val z) -> ArithEval st (arith_exp_id i)  z

  | arith_eval_plus : forall (e1 e2: ArithExp) (z1 z2: Integer), 
      ArithEval st e1 z1 -> ArithEval st e2 z2 -> ArithEval st (e1 + e2) (int_plus z1 z2) 

  | arith_eval_minus : forall (e1 e2: ArithExp) (z1 z2: Integer), 
      ArithEval st e1 z1 -> ArithEval st e2 z2 -> ArithEval st (e1 - e2) (int_minus z1 z2) 

  | arith_eval_mult : forall (e1 e2: ArithExp) (z1 z2: Integer), 
      ArithEval st e1 z1 -> ArithEval st e2 z2 -> ArithEval st (e1 * e2) (int_mult z1 z2)

  | arith_eval_div : forall (e1 e2: ArithExp) (z1 z2: Integer),
      ArithEval st e1 z1 -> ArithEval st e2 z2 -> ArithEval st (e1 / e2) (int_div z1 z2)

  | arith_eval_mod : forall (e1 e2: ArithExp) (z1 z2: Integer),
      ArithEval st e1 z1 -> ArithEval st e2 z2 -> ArithEval st (e1 mod e2) (int_modulo z1 z2)
.

Inductive MatrixEval (st: State)(m n: Integer) : MatrixExp -> Matrix Byte m n -> Prop :=
  | matrix_eval_lit : forall (matr: Matrix Byte m n),
      MatrixEval st matr matr
  
  | matrix_eval_id : forall (i: Id)(matr: Matrix Byte m n),
    st i = Some (byte_matrix_val matr) -> MatrixEval st i matr

  | matrix_eval_init : forall (e1 e2: ArithExp)(b: Byte),
                       ArithEval st e1 m -> ArithEval st e2 n ->
                       MatrixEval st (matrix_exp_init e1 e2) (matrix_zero b m n)
.

Inductive ByteEval (st: State) : ByteExp -> option Byte -> Prop :=
  | byte_eval_lit : forall (b: Byte),
      ByteEval st b (Some b)

  | byte_eval_id : forall (i: Id)(b: Byte),
      st i = Some (byte_val b) -> ByteEval st i (Some b)

  | byte_eval_xor : forall (e1 e2: ByteExp)(b1 b2: Byte),
      ByteEval st e1 (Some b1) -> ByteEval st e2 (Some b2) -> ByteEval st (e1 xor e2) (Some (byte_xor b1 b2))

   | byte_eval_andbb : forall (e1 e2: ByteExp)(b1 b2: Byte),
      ByteEval st e1 (Some b1) -> ByteEval st e2 (Some b2) -> ByteEval st (e1 band e2) (Some (byte_and b1 b2))

  | byte_eval_shiftl : forall (e: ByteExp)(x: Integer)(n: ArithExp)(b: Byte),
      ByteEval st e (Some b) -> ArithEval st n x -> ByteEval st (e shl n) (Some (byte_shl b x))

  | byte_eval_shiftr : forall (e: ByteExp)(x: Integer)(n: ArithExp)(b: Byte),
      ByteEval st e (Some b) -> ArithEval st n x -> ByteEval st (e shr n) (Some (byte_shr b x))

  | byte_eval_matrix : forall e1 e2 (m n i j: Integer)(mexp: MatrixExp)(matr: Matrix Byte m n),
                       MatrixEval st mexp matr -> ArithEval st e1 i -> ArithEval st e2 j ->
                       ByteEval st (mexp[e1][e2]) (matrix_get i j matr)
.

(* Evaluacion de expresiones booleanas *)
Inductive BoolEval (st: State) : BoolExp -> Bool -> Prop :=
  | bool_eval_lit : forall (b: Bool),
      BoolEval st b b

  | bool_eval_id  : forall (i: Id)(b: Bool),
       st i = Some (bool_val b) ->  BoolEval st i b

  | bool_eval_eq  : forall (e1 e2: ArithExp)(n1 n2: Integer),
      ArithEval st e1 n1 -> ArithEval st e2 n2 -> BoolEval st (e1 == e2) (int_eq n1 n2)

  | bool_eval_lt  : forall (e1 e2: ArithExp)(n1 n2: Integer),
      ArithEval st e1 n1 -> ArithEval st e2 n2 -> BoolEval st (e1 lt e2) (int_lt n1 n2)

  | bool_eval_le  : forall (e1 e2: ArithExp)(n1 n2: Integer),
      ArithEval st e1 n1 -> ArithEval st e2 n2 -> BoolEval st (e1 le e2) (int_le n1 n2)

  | bool_eval_gt  : forall (e1 e2: ArithExp)(n1 n2: Integer),
      ArithEval st e1 n1 -> ArithEval st e2 n2 -> BoolEval st (e1 gt e2) (int_gt n1 n2)

 | bool_eval_gtb  : forall (e1 e2: ByteExp)(n1 n2: Byte),
      ByteEval st e1 (Some n1) -> ByteEval st e2 (Some n2) -> BoolEval st (e1 gtb e2) (byte_gt n1 n2)
 
 | bool_eval_eqb  : forall (e1 e2: ByteExp)(n1 n2: Byte),
      ByteEval st e1 (Some n1) -> ByteEval st e2 (Some n2) -> BoolEval st (e1 b== e2) (byte_eq n1 n2)

  | bool_eval_ge  : forall (e1 e2: ArithExp)(n1 n2: Integer),
      ArithEval st e1 n1 -> ArithEval st e2 n2 -> BoolEval st (e1 ge e2) (int_ge n1 n2)

  | bool_eval_not : forall (e: BoolExp)(b: Bool),
      BoolEval st e b -> BoolEval st (!e) (bool_not b)

  | bool_eval_and : forall (e1 e2: BoolExp)(b1 b2: Bool),
      BoolEval st e1 b1 -> BoolEval st e2 b2 -> BoolEval st (e1 and e2) (bool_and b1 b2)

  | bool_eval_or  : forall (e1 e2: BoolExp)(b1 b2: Bool),
      BoolEval st e1 b1 -> BoolEval st e2 b2 -> BoolEval st (e1 or e2) (bool_or b1 b2)
.

(* Instrucciones *)
Inductive Instr : Type :=
  | instr_skip          : Instr
  | instr_assign_bool   : Id      -> BoolExp   -> Instr
  | instr_assign_int    : Id      -> ArithExp  -> Instr
  | instr_assign_byte   : Id      -> ByteExp   -> Instr
  | instr_assign_matrix : Id      -> MatrixExp -> Instr
  | instr_seq           : Instr   -> Instr     -> Instr
  | instr_if            : BoolExp -> Instr     -> Instr -> Instr
  | instr_while         : BoolExp -> Instr     -> Instr
  | instr_for           : Id      -> ArithExp  -> Instr -> Instr
  | instr_matrix_set    : Id      -> ArithExp  -> ArithExp -> ByteExp -> Instr
.

Notation "'SKIP'" := instr_skip : lang_scope.

Notation "'bool'   X ::= a" := (instr_assign_bool   X a) (at level 80) : lang_scope.
Notation "'int'    X ::= a" := (instr_assign_int    X a) (at level 80) : lang_scope.
Notation "'byte'   X ::= a" := (instr_assign_byte   X a) (at level 80) : lang_scope.
Notation "'matrix' X ::= a" := (instr_assign_matrix X a) (at level 80) : lang_scope.

Notation "m [ i ][ j ] ::= x" := (instr_matrix_set m i j x) (at level 30, x at level 60) : lang_scope.

Notation "c1 ; c2" := (instr_seq c1 c2) (at level 80, right associativity) : lang_scope.
Notation "c1 ;" := (c1) (at level 80, right associativity) : lang_scope.

Notation "'WHILE' b 'DO' c 'END'" := (instr_while b c) (at level 80, right associativity) : lang_scope.
Notation "'FOR' b 'TO' c 'DO' d 'END'" := (instr_for b c d) (at level 80, right associativity) : lang_scope.
Notation "'IFB' c1 'THEN' c2 'ELSE' c3 'END'" := (instr_if c1 c2 c3)(at level 80, right associativity) : lang_scope.
Notation "'IFB' e1 'THEN' e2 'END'" := (IFB e1 THEN e2 ELSE SKIP END) (at level 80, right associativity) : lang_scope.

Reserved Notation "st $ c => st'" (at level 90, c at level 89).

Inductive InstrEval (st: State) : Instr -> State -> Prop :=
  | skip_eval :
      st $ SKIP => st

  | assign_bool_eval : forall bid bexp b,
      BoolEval st bexp b -> st $ bool bid ::= bexp => update st bid (bool_val b)

  | assign_int_eval : forall zid zexp z,
      ArithEval st zexp z -> st $ int zid ::= zexp => (update st zid (int_val z))

  | assign_byte_eval : forall bid bexp b,
      ByteEval st bexp (Some b) -> InstrEval st (byte bid ::= bexp) (update st bid (byte_val b))

  | assign_matrix_eval : forall mid (m n: Integer) (matr: Matrix Byte m n) (mexp : MatrixExp),
      MatrixEval st mexp matr -> st $ matrix mid ::= mexp => update st mid (byte_matrix_val matr)

  | seq_eval : forall instr1 instr2 st' st'',
      st $ instr1 => st' -> st' $ instr2 => st'' -> st $ instr1; instr2 => st''

  | if_eval_true : forall bexp instr1 instr2 st',
      BoolEval st bexp TRUE -> st $ instr1 => st' ->
      st $ IFB bexp THEN instr1 ELSE instr2 END => st'

  | if_eval_false : forall bexp instr1 instr2 st',
      BoolEval st bexp FALSE -> st $ instr2 => st' ->
      st $ IFB bexp THEN instr1 ELSE instr2 END => st'

  | while_eval_true : forall bexp instr st' st'',
      BoolEval st bexp TRUE -> st $ instr => st' -> st' $ WHILE bexp DO instr END => st'' ->
      st $ WHILE bexp DO instr END => st''

  | while_eval_false : forall bexp instr,
      BoolEval st bexp FALSE -> st $ WHILE bexp DO instr END => st

  | for_eval_end : forall (i: Id) n instr,
      BoolEval st (i ge n) TRUE -> st $ FOR i TO n DO instr END => st

  | for_eval_step : forall (i: Id) x n instr st' st'',
      BoolEval st (i lt n) TRUE -> st $ instr => st' -> 
      st' $ (FOR i TO n DO instr END) => st'' -> st' i = Some (int_val x) ->
      st'' i = Some (int_val (int_plus x ONE)) ->
      st $ (FOR i TO n DO instr END) => st''

  | matrix_set_eval : forall m n i j e1 e2 e (mid: Id) (matr matr': Matrix Byte m n) b,
      MatrixEval st mid matr -> ArithEval st e1 i -> ArithEval st e2 j -> ByteEval st e (Some b) ->
      matrix_set matr i j b = Some matr' ->
      st $ mid[e1][e2] ::= e => update st mid (byte_matrix_val matr')

  where "st $ c => st'" := (InstrEval st c st')
.

End Lang.
